$\forall$${\it da}$:$k$:Knd fp$\rightarrow$ Type, $k$:\{$k$:Knd$\mid$ $k$ $\in$ dom(${\it da}$) \& isrcv($k$) \}. da{-}outlink{-}f(${\it da}$;$k$) $\in$ IdLnk$\times$Id$\times$Type